\asegura{res==(\exists r_1,r_2 \selec resNoCon(h,d), r_1 \neq r_2) seSolapan(r_1,r_2)}

\aux{resNoCon}{h:Hotel,d:DNI}{[Reservas]}{[ x | x \selec reservas(h), documento(x)==d, confirmada(x)==False]}

\aux{seSuperponen}{a,b:[\ent]}{\bool}{ |[x | x \selec a, x \in b] | > 0}

\aux{seSolapan}{r1,r2:Reserva}{\bool}{seSuperponen(\rango{fechaDesde( r1 )}{fechaHasta(r1)} , \rango{fechaDesde(r2)}{fechaHasta(r2)})}

